• Chor  chorName{
•     Main() = Exp1;
•     P(x1, x2, ..., xn) = Exp2;
•     ...
• }

where P is the process name, x1, ..., xn is an optional list of process parameters and Exp is a process expression. The process expression determines the computational logic of the process. A process without parameters is written either as P() or P. A defined process may be referenced by its name (with the valuations of the parameters). Process referencing allows a flexible form of recursion. Inside a choreography, one of the process must have name "Main" with no parameter, which acts like the starting process of the choreography. 

Each expression can be composed by using the following operators.

Stop

The deadlock process is written as follows,

Stop

The process does absolutely nothing.

Skip

The process which terminates immediately is written as follows,

Skip

The process terminates and then behaves exactly the same as Stop.

Service Invocation

In choreography, one role inside the service can invoke the service provided by another role. We assume that each role is associated with a set of local variables and there are no globally shared variables among roles. This is a reasonable assumption as each role (which is a service) may be realized in a remote computing device. One example of service invocation is the following:

channel B2S ; //The pre-established channel between the buyer and the seller

B2S(Buyer, Seller, {Bch})  -> Skip

The above states that role Buyer invokes a service provided by role Seller through channel B2S.  {Bch} is a sequence of session channels which are created for this service invocation only. Notice that because the same service shall be available all the time, service channel B2S is reserved for service invocation only.

Channel Communication

Once the service channel is established between two roles, the two roles can communication using the channel agreed in the service invocation. The following two example demonstrates the idea.

Bch(Buyer, Seller, QuoteRequest) -> Skip
      Bch(Seller, Buyer, QuoteResponse.x) -> Skip

In the first example, Buyer sends a message QuoteRequest to Seller. In the second exmaple, Seller sends a QuoteResponse to Buyer with the quotation value x. Variable x is associated with role Buyer and can be used inside the choreography afterwards as a variable of role Buyer.

Assignment

We support the update of the variables of a role. Without loss of generality, we always require that the variables constituting new value and the variable to be updated must be associated with the same role. The following example demonstrated the usage of assignment.

A2A(TravelAgent, AmericanAirlines, {ch}) -> ch(AmericanAirlines, TravelAgent, FlightResponseAA.price) -> (TravelAgent.p = price *1.1)-> Skip

TravelAgent invokes the service provided by AmericanAirlines, then AmericanAirlines gives a flight quotation to TravelAgent stored in variable price. TravelAgent needs to calculate the price displayed to the client by adding profits. Both variable p and price are the variables of role TravelAgent .

Sequential composition

A sequential composition is written as,

P; Q

where P and Q are processes. In this process, P starts first and Q starts only when P has finished.

Choice

In Web Service module, we have only external choice, which is made by the environment, e.g., the observation of a visible event or the valuation of the variables. An choice is written as follows,

P [] Q

The choice operator [] states that either P or Q may execute. If P performs a visible event first, then P takes control. Otherwise, Q takes control.

The generalized form of choice is written as,

[] x:{1..n}@ P(x)                                - which is equivalent to P(1) [] ... [] P(n)

Conditional Choice

A choice may depend on a Boolean expression which in turn depends on the valuations of the variables. In PAT, we support the classic if-then-else as follows,

if (cond) { P } else { Q }

where cond is a Boolean formula. If cond evaluates to be true, then P executes, otherwise Q executes. Notice that the else-part is optional. The process if(false) {P} behaves exactly as process Skip.

Case

A generalized form of conditional choice is written as,

• case {
•     cond1: P1
•     cond2: P2
•     default: P
• }

where case is a key word and cond1, cond2 are Boolean expressions. if cond1 is true, then P1 executes. Otherwise, if cond2 is true, then P2. And if cond1 and cond2 are both false, then P executes by default. The condition is evaluated one by one until a true one is found. In case no condition is true, the default process will be executed. 

Guarded process

A guarded process only executes when its guard condition is satisfied. In PAT, a guard process is written as follows,

[cond] P

where cond is a Boolean formula and P is a process. If cond is true, P executes. Notice that different from conditional choice, if cond is false, the whole process will wait until cond is true and then P executes. 

Interleaving

Two processes which run concurrently without barrier synchronization written as,

P ||| Q

where ||| denotes interleaving. Both P and Q may perform their local actions without referring to each other. Notice that P and Q can still communicate via shared variables or channels. The generalized form of interleaving is written as,

||| x:{0..n} @ P(x)

Recursion

Recursion is achieved through process referencing flexibly. The following process contains mutual recursion.

• P() = a -> Q();
• Q() = b -> P();
• System() = P() || Q();

It is straightforward to use process reference to realize common iterative procedures. For instance, the following process behaves exactly as while (cond) {P()};

Q() = if (cond) {P(); Q()};